(set-logic ALL)
(set-info :status sat)
(declare-sort S 0)
(declare-datatype Option (par (X) ( (none) (some (val X)))))
(declare-const x (Option S))
(declare-const y (Option S))
(assert (= x y))
(check-sat)
(exit)
